The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(=(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
f(x, g(y, z)) →⁺ g(f(x, y), z)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [y / g(y, z)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(='(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(='(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)

Types:
f :: max':u → nil:g → nil:g
nil :: nil:g
g :: nil:g → max':u → nil:g
++ :: nil:g → nil:g → nil:g
null :: nil:g → true:false:or:not
true :: true:false:or:not
false :: true:false:or:not
mem :: nil:g → max':u → true:false:or:not
or :: =' → true:false:or:not → true:false:or:not
=' :: max':u → max':u → ='
max :: nil:g → max':u
not :: true:false:or:not → true:false:or:not
max' :: max':u → max':u → max':u
u :: max':u
hole_nil:g1_0 :: nil:g
hole_max':u2_0 :: max':u
hole_true:false:or:not3_0 :: true:false:or:not
hole_='4_0 :: ='
gen_nil:g5_0 :: Nat → nil:g
gen_max':u6_0 :: Nat → max':u
gen_true:false:or:not7_0 :: Nat → true:false:or:not

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
f, ++, mem, max

(8) Obligation:

TRS:
Rules:
f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(='(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)

Types:
f :: max':u → nil:g → nil:g
nil :: nil:g
g :: nil:g → max':u → nil:g
++ :: nil:g → nil:g → nil:g
null :: nil:g → true:false:or:not
true :: true:false:or:not
false :: true:false:or:not
mem :: nil:g → max':u → true:false:or:not
or :: =' → true:false:or:not → true:false:or:not
=' :: max':u → max':u → ='
max :: nil:g → max':u
not :: true:false:or:not → true:false:or:not
max' :: max':u → max':u → max':u
u :: max':u
hole_nil:g1_0 :: nil:g
hole_max':u2_0 :: max':u
hole_true:false:or:not3_0 :: true:false:or:not
hole_='4_0 :: ='
gen_nil:g5_0 :: Nat → nil:g
gen_max':u6_0 :: Nat → max':u
gen_true:false:or:not7_0 :: Nat → true:false:or:not

Generator Equations:
gen_nil:g5_0(0) ⇔ nil
gen_nil:g5_0(+(x, 1)) ⇔ g(gen_nil:g5_0(x), u)
gen_max':u6_0(0) ⇔ u
gen_max':u6_0(+(x, 1)) ⇔ max'(u, gen_max':u6_0(x))
gen_true:false:or:not7_0(0) ⇔ true
gen_true:false:or:not7_0(+(x, 1)) ⇔ or(='(u, u), gen_true:false:or:not7_0(x))

The following defined symbols remain to be analysed:
f, ++, mem, max